Nuprl Definition : R-self-interface 11,40

R-self-interface(R)
== es_realizer_ind(R;
== es_realizer_ind(True;
== es_realizer_ind(left,right,rec1,rec2.(rec1  rec2);
== es_realizer_ind(loc,T,x,v.True;
== es_realizer_ind(loc,T,x,L.True;
== es_realizer_ind(lnk,tag,L.True;
== es_realizer_ind(loc,ds,knd,T,x,f.True;
== es_realizer_ind(ds,knd,T,l,dt,g.((isrcv(knd))
== es_realizer_ind( (lnk(knd) = l)
== es_realizer_ind( subtype_rel(fpf-cap(dt; id-deq; tag(knd); void); T));
== es_realizer_ind(loc,ds,a,T,P.True;
== es_realizer_ind(loc,k,L.True;
== es_realizer_ind(loc,k,L.True;
== es_realizer_ind(loc,x,L.True) 
latex



clarification:

R-self-interface(R)
== es_realizer_ind(R;
== es_realizer_ind(True;
== es_realizer_ind(left,right,rec1,rec2.(rec1  rec2);
== es_realizer_ind(loc,T,x,v.True;
== es_realizer_ind(loc,T,x,L.True;
== es_realizer_ind(lnk,tag,L.True;
== es_realizer_ind(loc,ds,knd,T,x,f.True;
== es_realizer_ind(ds,knd,T,l,dt,g.((isrcv(knd))
== es_realizer_ind( (lnk(knd) = l  IdLnk)
== es_realizer_ind( subtype_rel(fpf-cap(dt; id-deq; tag(knd); void); T));
== es_realizer_ind(loc,ds,a,T,P.True;
== es_realizer_ind(loc,k,L.True;
== es_realizer_ind(loc,k,L.True;
== es_realizer_ind(loc,x,L.True) 
latex


Definitionses realizer ind, P  Q, b, isrcv(k), P  Q, s = t, IdLnk, lnk(k), fpf-cap(feqxz), id-deq, tag(k), void, True
FDL editor aliasesR-self-interface

origin